i, j:Id, k1, k2:Knd. (isrcv(k1))  (k1 = k2)  (locknd(i;k1) = locknd(j;k2)  LocKnd) 

latex

Definitions	x:A. B(x), P  Q, SQType(T), {T}, t  T, , rcv(l,tg), lnk(k), LocKnd, locknd(i;k), kindcase(k; a.f(a); l,t.g(l;t) ), t.1, outl(x), if b then t else f fi , islocal(k), b, isl(x), tt, ff, P  Q, P  Q, P & Q
Lemmas	Knd sq, isrcv-implies, Knd wf, assert wf, isrcv wf, Id wf, ldst wf, lnk wf, hasloc wf, assert-hasloc